\begin{tabbing} $\vdash$ \=$\forall$$A$, $B$, $C$:Type, $g$:($A$$\rightarrow$($B$ + Top)), $f$:($B$$\rightarrow$($C$ + Top)), $x$:$A$.\+ \\[0ex]($\uparrow$can{-}apply($f$ o $g$ ;$x$)) $\Leftarrow\!\Rightarrow$ (($\uparrow$can{-}apply($g$;$x$)) \& ($\uparrow$can{-}apply($f$;do{-}apply($g$;$x$)))) \- \end{tabbing}